Рантайм библиотека на Coq

Одно из заданий диссертации, построение рантайм библиотеки компактнее всего
можно сформулировать вот так:

CoREPL> spawn ack 4 1
20
CoREPL> spawn ack 4 1
21
CoREPL> ls
[(20,ack,10043),(21,ack,10033)]
20:65533
21:65533
CoREPL> kill 20
Ok
CoREPL> send 20 "hello"
Error
CoREPL>


Вот такое написать — уже неплохая цель, думаю даже больше будет чем любые
другие а ля VM на Coq. Странно конечно звучит писать обычные программы, а в
полях держать поля username и password в теоремах, но почему нет?

В такое я думаю трансформировать со временем https://github.com/5HT/co
Кто там хотел в Групоид Инфинити, приходите писать на Coq будет весело
https://gitter.im/groupoid/exe
Денег нет, популярности нет, чистейшее R&D под ваши нужды, предлагайте свои
идеи, будем в эту сторону двигать! Область наших интересов в этом проекте:
стрим процессинг, векторизация, стрим фьюжин (т.е. с вероятностью > 1/2 то же,
чем вы занимаетесь у себя на производстве) компиляция в LLVM языки — точка
соприкосновения с http://groupoid.space/hnc. Этот проект назовем в будущем
условно co — такого двухбуквенного сочетания в домене проектов нашей вселенной
Marvell еще не было — REPL интерпретатор и рантайм система для программирования
на Coq.